Nuprl Lemma : comb_for_inl_wf
4,23
postcript
pdf
(
x
,
z
. inl(
x
))
Top
True
Decision
latex
Definitions
T
,
x
:
A
.
B
(
x
)
,
t
T
,
True
,
Top
Lemmas
top
wf
,
true
wf
,
squash
wf
,
inl
wf
origin
x,z. inl(x)) 
Top
TrueDecision x,z. inl(x)) TopTrueDecision T
x:A. B(x) T